\begin{nusmvCommand} {gen\_ltlspec\_bmc} {Dumps into one or more dimacs files the given LTL specification, or all LTL specifications if no formula is given. Generation and dumping parameters are the maximum bound and the loopback value}

\cmdLine{gen\_ltlspec\_bmc [-h | -n idx | -p "formula" [IN context]] \linebreak[4][-k max\_length] [-l loopback] [-o filename]}

This command generates one or more problems, and  dumps each problem
into a dimacs file. Each problem is related to a specific problem
bound, which increases from zero (0) to the given maximum problem
bound. In this short description \code{length} is the bound of the
problem that system is going to dump out. 

In this context the maximum problem bound is represented by the {\it
max\_length} parameter, or by its default value stored in the
environment variable \envvar{bmc\_length}.

Each dumped problem also depends on the loopback you can explicitly
specify by the \commandopt{l} option, or by its default value stored
in the environment variable \envvar{bmc\_loopback}.

The property to be checked may be specified using the \commandopt{n
idx} or the \commandopt{p "\anyexpr"} options.

You may specify dimacs file name by using the option \commandopt{o
\filename{filename}}, otherwise the default value stored in the environment
variable \envvar{bmc\_dimacs\_filename} will be considered.

\begin{cmdOpt}
\opt{-n \parameter{\natnum{\it index}}}{ {\it index} is the numeric index of a valid LTL
specification formula actually located in the properties database.
The validity of \code{index} value is checked out by the system.  }

\opt{-p \parameter{"\anyexpr [IN context]"}}{ Checks the \anyexpr specified
on the command-line. \code{context} is the module instance name which
the variables in  \anyexpr must be evaluated in.}
            
\opt{-k \parameter{\natnum{\it max\_length}}}{ {\it max\_length} is the maximum problem
bound used when increasing problem bound starting from zero. Only
natural numbers are valid values for this option. If no value is given
the environment variable {\it bmc\_length} value is considered
instead.}
       
\opt{-l \parameter{\set{\it loopback}{\range{0}{max\_length-1},
 \range{-1}{-bmc\_length}, X, *}}}{The {\it loopback} value may be:}
 \tabItem{a natural number in (0, {\it max\_length-1}). A positive sign ('+') can 
       be also used as prefix of the number. Any invalid combination of bound 
       and loopback will be skipped during the generation and 
       dumping process.}
  \tabItem{a negative number in (-1, -{\it bmc\_length}). In this case 
       {\it loopback} is considered a value relative to {\it max\_length}. 
       Any invalid combination of bound and loopback will be skipped during 
       the generation process.}
  \tabItem{the symbol `\varvalue{X}', which means ``no loopback". }
  \tabItem{the symbol `\varvalue{*}', which means ``all possible loopback from zero to 
       {\it length-1}".}

\opt{-o \parameter{\filename{\it filename}}}{ {\it filename} is the name of dumped dimacs
files. If this options is not specified, variable {\it
bmc\_dimacs\_filename} will be considered. The file name string may
contain special symbols which will be macro-expanded to form the real
file name.  Possible symbols are: }
       \tabItem{@F: model name with path part.} 
       \tabItem{@f: model name without path part.} 
       \tabItem{@k: current problem bound.} 
       \tabItem{@l: current loopback value .}
       \tabItem{@n: index of the currently processed formula in the property 
       database.} 
       \tabItem{@@: the `@' character.}
\end{cmdOpt}
\end{nusmvCommand}
